section "Example: Quicksort on Heap Lists"

theory k_mem_pool_simpl
imports "./lib/simpl/Vcg" "./lib/simpl/HeapList" "HOL-Library.Permutation"
begin

record globals_dlist =
  head_' :: "ref \<Rightarrow> ref"
  next_' :: "ref \<Rightarrow> ref"
  tail_' :: "ref \<Rightarrow> ref"
  prev_' :: "ref \<Rightarrow> ref"

record globals_k_mem_pool_lvl =
  bits_' :: "ref \<Rightarrow> nat"
  bits_p_' :: "ref \<Rightarrow> nat list"
  free_list_' :: "ref \<Rightarrow> ref"  

record globals_k_mem_pool = 
  buf_' :: "ref \<Rightarrow> ref list"
  max_sz_' :: "ref \<Rightarrow> nat"
  n_max_' :: "ref \<Rightarrow> nat"
  n_levels_' :: "ref \<Rightarrow> nat"
  max_inline_level_' :: "ref \<Rightarrow> nat"
  levels_' :: "ref \<Rightarrow> ref list"
  wait_q_' :: "ref \<Rightarrow> ref"

hoarestate kstate = 
  A :: nat
  I :: nat
  N :: nat
  M :: nat

record 'g vars = "'g state" +
  list_' :: "ref"
  node_' :: "ref"
  ret_bool_' :: bool
  (*  static void *block_ptr(struct k_mem_pool *p, size_t lsz, int block)  *)
  p_'    :: "ref"
  lsz_'  :: "nat"
  int_block_' :: "nat"
  ret_ref_' :: "ref"
  (*  static int block_num(struct k_mem_pool *p, void *block, int sz)  *)
  block_' :: "ref"
  sz_' :: "nat"
  ret_block_num_' :: "nat"
  (*  static void set_free_bit(struct k_mem_pool *p, int level, int bn)  *)
  level_'    :: "nat"
  bn_'    :: "nat"
  bit_array_index_' :: "nat"
  bit_array_' :: "nat list"
  pool_level_' :: "ref"
  r_'    :: "nat"
  N_'    :: "nat"
  R_'    :: "nat"

procedures
  sys_dlist_init(list) = 
  "\<acute>list\<rightarrow>\<acute>head :== \<acute>list;;
   \<acute>list\<rightarrow>\<acute>tail :== \<acute>list "

procedures
  sys_dlist_is_head(list, node|ret_bool) = 
  "IF \<acute>list\<rightarrow>\<acute>head = \<acute>node
    THEN \<acute>ret_bool :== True
    ELSE \<acute>ret_bool :== False
   FI"

procedures
  sys_dlist_is_tail(list, node|ret_bool) = 
  "IF \<acute>list\<rightarrow>\<acute>tail = \<acute>node
    THEN \<acute>ret_bool :== True
    ELSE \<acute>ret_bool :== False
   FI"
  
procedures
  sys_dlist_is_empty(list|ret_bool) = 
  "IF \<acute>list\<rightarrow>\<acute>tail = \<acute>list
    THEN \<acute>ret_bool :== True
    ELSE \<acute>ret_bool :== False
   FI"

procedures
  sys_dlist_append(list, node) = 
  " \<acute>node\<rightarrow>\<acute>next :== \<acute>list;;
    \<acute>node\<rightarrow>\<acute>prev :== \<acute>list\<rightarrow>\<acute>tail;;
    \<acute>list\<rightarrow>\<acute>tail\<rightarrow>\<acute>next :== \<acute>node;;
    \<acute>list\<rightarrow>\<acute>tail :== \<acute>node"

procedures
  sys_dlist_remove(node) = 
  " \<acute>node\<rightarrow>\<acute>prev\<rightarrow>\<acute>next :== \<acute>node\<rightarrow>\<acute>next;;
    \<acute>node\<rightarrow>\<acute>next\<rightarrow>\<acute>prev :== \<acute>node\<rightarrow>\<acute>prev"

procedures
  sys_dlist_peek_head(list|node) = 
  "\<acute>ret_bool :== CALL sys_dlist_is_empty(\<acute>list);;
    IF (\<acute>ret_bool)
      THEN \<acute>node :== Null
      ELSE \<acute>node :== \<acute>list
    FI"

procedures
  sys_dlist_get(list|node) = 
  "\<acute>ret_bool :== CALL sys_dlist_is_empty(\<acute>list);;
    IF (\<acute>ret_bool)
      THEN  \<acute>node :== Null
      ELSE  \<acute>node :== \<acute>list \<rightarrow>\<acute>head;;
            CALL sys_dlist_remove(\<acute>node)
    FI"

(*
sys_dlist_init
sys_dlist_append
sys_dlist_get
sys_dlist_remove
sys_dlist_peek_head
*)

procedures
  block_ptr(p, lsz, int_block | ret_ref) =      
  " \<acute>ret_ref :== \<acute>p\<rightarrow>\<acute>buf ! (\<acute>lsz*\<acute>int_block)"

procedures
  block_num(p, block, sz | ret_block_num) =      
  " \<acute>ret_block_num :== length (\<acute>p\<rightarrow>\<acute>buf) "

procedures
  set_free_bit(p, level, bn) =      
  " \<acute>bit_array_index :== \<acute>bn div 32;;
    \<acute>pool_level :== (\<acute>p\<rightarrow>\<acute>levels) ! \<acute>level
  "


(**
procedures
  Fac (N|R) = "IF \<acute>N = 0 THEN \<acute>R :== 1
                       ELSE \<acute>R :== CALL Fac(\<acute>N - 1);;
                            \<acute>R :== \<acute>N * \<acute>R
                       FI"

procedures
  compare_two(p|r) = 
(**    "IF 'p \<le> 'q then 'p :== 'p ELSE 'p :== 'q FI"**)
  "\<acute>r :== \<acute>p"
**)

end
